#define _GNU_SOURCE
#include <stdio.h>
#include <stdlib.h>
#include <termios.h>
#include <unistd.h>
#include <sys/ioctl.h>
#include <assert.h>

#ifdef __VERIFY
_Bool nondet_bool ();

void *my_malloc (size_t s)
{
	if (nondet_bool ()) { return (NULL);};
	return (malloc (s));
}
#else
void *my_malloc (size_t s)
{
	return (malloc (s));
}
#endif

struct stack{
	struct stack_element* top;
};
struct stack_element{
	struct stack_element* prev;
	int number;
};

struct stack* new_stack(){
	struct stack* stack = (struct stack*)my_malloc(sizeof(struct stack));
	stack->top = NULL;
	return stack;
}
void push(int value, struct stack* stack)
{
	if(!stack) return;
	struct stack_element* el = (struct stack_element*) my_malloc(sizeof(struct stack_element));
	if(!el) return;
	el->number = value;
	el->prev = stack->top;
	stack->top = el;
}
int pop(struct stack* stack){
	if(!stack) {
		exit(-1);
	}
	else if(!stack->top){
		printf("%s\n","Pop from an empty stack.");
		exit(-1);
	}
	else{
		struct stack_element* tmp = stack->top;
		int value = tmp->number;
		stack->top = tmp->prev;
		free(tmp);
		tmp = NULL;
		return value;
	}
}
void stack_test(){
	struct stack* stack = new_stack();
	int i = 0;
	for(;i<15;i++){
		push(i,stack);
	}
	printf("%s","pushed 15 elements\n");
	//pop and push test.
	assert(pop(stack)==14);
	push(14,stack);
	//stack order test
	int assert_value = 14;
	for(i=0;i<15;i++){
		int value = pop(stack);
		printf("%s ,%i\n","pop element:",value);
		assert(value == assert_value);
		assert_value--;
	}
	free(stack);
	stack = NULL;
}
int main(int argc, char **argv){
	const int ELEMNB = 1000;
	struct stack* stack = new_stack();
	int i = 0;
	for(;i<ELEMNB;i++){
		push(i,stack);
	}
	int assert_value = ELEMNB-1;
	for(i=0;i<ELEMNB;i++){
		int value = pop(stack);
		printf("%s ,%i\n","pop element:",value);
		assert(value == assert_value);
		assert_value--;
	}
	free(stack);
	stack = NULL;
	return(0);
}
